A:Type, eq:EqDecider(A), x:A, v, z:Top. x : v(x)?z ~ v 

latex

Definitions	f(x), Unit, P  Q, P & Q, b, b, A, False, , eqof(d), true, Top, EqDecider(T), x : v, f(x)?z, x  dom(f), Prop, SQType(T), P  Q, {T}, t  T, x:A. B(x)
Lemmas	btrue wf, eqof wf, bool sq, bool wf, deq wf, top wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity